da:fpf(Knd; k.Type). normal-da{i:l}(da)  prop{i:l} 

latex

Definitions	x:A. B(x), t  T, prop{i:l}, normal-da{i:l}(da), fpf-all(A; eq; f; x,v.P(x;v)), P  Q, x. t(x), x(s)
Lemmas	Knd wf, assert wf, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, normal-type wf, fpf-ap wf, fpf wf